% Poster for ME'12 by Qin ZHANG, Sep. 2012, SnT Unversity of Luxembourg
% by Qin ZHANG
% Security Design and Validation Research Group (SERVAL)
% SnT, University of Luxembourg
% Sep. 2012

\documentclass[final]{beamer}

\mode<presentation>
{  
  \usetheme{TUGraz}    
}

\usepackage{amsmath,amsthm, amssymb, latexsym}
\usepackage{multirow}
\usepackage{pifont}
\usepackage{algpseudocode}
\usepackage{colortbl}
\usepackage{booktabs, boxedminipage}
\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage{graphicx}
\usepackage{upgreek}
\usepackage[orientation=portrait,size=a0,scale=1.45,debug]{beamerposter}   

\title{Invariant Preservation in\\ Iterative Modeling}
\author[L\'ucio, Syriani, Amrani, Zhang \& Vangheluwe]{Levi L\'ucio, Eugene Syriani, Moussa Amrani,\\ Qin Zhang and Hans Vangheluwe}
\institute{\small MSDL, McGill University\\ SERVAL@SnT and LASSY, University of Luxembourg\\ SERG@CS, University of Alabama\\ AnSyMo, Antwerp University}
\mail{Contact: qin.zhang@uni.lu}
\webpage{\vspace{-0.5cm}\hspace{-1cm}\includegraphics[scale=0.6]{./logos/fnr.pdf}~This work was partially supported by the Luxembourgish \emph{Fonds National de la Recherche}. }

\DeclareMathOperator{\eqqdef}{\stackrel{\triangle}{=}}
\newcommand{\FS}{\ensuremath{\mathtt{FS}}}
\newcommand{\FSS}{\ensuremath{\mathtt{FS}_{\mathsf{s}}}}
\newcommand{\FSC}{\ensuremath{\mathtt{FS}_{\mathsf{c}}}}

\usebackgroundtemplate{	\includegraphics[width=\paperwidth]{bg.pdf}}

\begin{document}

\begin{frame}
\begin{center}

\begin{minipage}{0.98\textwidth}
	\begin{minipage}{0.49\textwidth}
		\begin{block}{1. Motivation}
			\begin{minipage}{\textwidth}
				\begin{minipage}{0.98\textwidth}
					\begin{description}
						\item[\textbf{Iterative Modeling \cite{Konrad2007}:}] a modeler tries to meet a given set of requirements, 
							by iteratively enhancing a model while satisfying a larger subset of requirements, until all of them are satisfied
						\item[\textbf{Property Preservation:}] How to ensure that a model $\mathtt{M_i}$, already satisfying a set of properties $P_i$, 
							evolves safely in a model $\mathtt{M_{i+1}}$ still satisfying these properties $\tau(P_i)$ adapted to $\mathtt{M_{i+1}}$, plus eventually new properties $P_{\mathsf{new}}$?
						\begin{center}
							$M_i \models P_i \rightarrow M_{i+1} \models \uptau (P_i) \wedge P_{new}$
						\end{center}	
						\item[\textbf{Proposal (Safe Iterative Evolution):}] Following our methodology, we ensure by \emph{construction} that evolution still preserves previous properties
					\end{description}
				
					\medskip
					\hspace{-0.6em}
					\begin{minipage}{0.98\textwidth}
						\begin{minipage}{0.63\textwidth}
							\begin{enumerate}
								\item Specify the system using a Domain-Specific Metamodel (\textsc{Dsm}), and the corresponding requirements;
								\item Translate the metamodel (i.e. data and semantics) into an Algebraic Petri Net (\textsc{Apn}), and the requirements as \textsc{Apn} invariants;
							\end{enumerate}
						\end{minipage}
						\hfill
						\begin{minipage}{0.35\textwidth}
							\begin{figure}
								\includegraphics[scale=4.5]{figures/Iiter-modeling}
							\end{figure}
						\end{minipage}
					\end{minipage}	
				\end{minipage}
			\end{minipage}
		\end{block}
	\end{minipage}	
	\hfill	
	\begin{minipage}{0.49\textwidth}
		\begin{block}{2. Running Example}
		\begin{minipage}{0.98\textwidth}
			\begin{minipage}{0.54\textwidth}
				\textbf{Multi-Level Security File System} (\textsc{Mls}) \cite{ASSE:Cristia}: 
					\begin{description}
						\small
						\item[Users] can request access to files, in read or write mode;
						\item[Files] represent system resources;
						\item[Access Classes] attached to users and files, encode access control through security level and category credentials.
					\end{description}
				\end{minipage}
				\hfill
				\begin{minipage}{0.44\textwidth}
					\begin{figure}% Change the figure to include only the memtamodel
						\includegraphics[width=\textwidth]{figures/metamodel}
					\end{figure}
				\end{minipage}
			\end{minipage}	
			
			\hfill \\  \normalsize
			\medskip
			\vspace{0.6em}
		
			\begin{minipage}{0.98\textwidth}
				\begin{minipage}{0.59\textwidth}
					\textbf{Model Transformation} in two steps:
					\begin{enumerate}
						\small				
						\item Data structures expressed by the metamodel and the model at hand are translated into Algebraic Specifications: 
							the metamodel defines the signatures and operations; the data from the model specify a particular term, like the one in the right;
						\item The metamodel's semantics is encoding by translation to \textsc{Apn}s (cf. \S 5) 
					\end{enumerate} 
				\end{minipage}	
				\hfill	
				\begin{minipage}{0.37\textwidth}
					\begin{tabular}{@{}c | @{}c@{} | c |@{}c@{}}
 						& Name & $\mathtt{SL}$ & $\mathtt{CR}$\\\hline\hline
						\multirow{3}{*}{\rotatebox{90}{Files}}
 						& $\mathtt{f1}$     &     2       & $\mathtt{NATO}$\\
 						& $\mathtt{f2}$     &     0       & $\mathtt{CIA}$\\
 						& $\mathtt{f3}$     &     1       & $\emptyset$\\\hline
						\multirow{3}{*}{\rotatebox{90}{Users}}
 						& $\mathtt{levi}$   &     3       & $\,\mathtt{NATO}, \mathtt{CIA}\,$\\
 						& $\mathtt{\,eugene\,}$ &     0       & $\,\mathtt{NATO}, \mathtt{CIA}\,$\\
					\end{tabular}
				\end{minipage}
			\end{minipage}
		\end{block}
	\end{minipage}	
\end{minipage}

\hfill

\begin{minipage}{0.98\textwidth}
	\begin{minipage}{0.49\textwidth}
		\begin{block}{3. System Requirements}
			Requirements are derived from the \textsc{Dsm} to ensure a correct semantics for the \textsc{Apn}. For the \textsc{Mls}, two requirements (\textbf{\texttt{R1}}), (\textbf{\texttt{R2}}), are later translated into three properties $\mathtt{P1}, \mathtt{P2}, \mathtt{P3}$ over the resulting \textsc{Apn} as follows:
			
			\begin{description}
				\item[\texttt{R1}:] A file can be open, either in read or in write mode, only by a user with sufficient access rights
					$$\begin{array}{r @{~\eqqdef~} l}
						\mathtt{P1}  & \forall~ \mathtt{\$p} = (\mathtt{\$f}, \mathtt{\$u}) \in \mathtt{writing} \cdot \mathtt{ac_{u}} \rhd \mathtt{ac_{f}}\\
						\mathtt{P2}  & \forall~ \mathtt{\$p} = (\mathtt{\$f}, \mathtt{\$u}) \in \mathtt{reading} \cdot \mathtt{ac_{u}} \rhd \mathtt{ac_{f}}\\
					\end{array}$$
			
				\item[\texttt{R2}:]  A user always respects the data confinement condition, i.e. the user cannot open a file with lower \emph{confidentiality} in write mode while opening a file with higher \emph{confidentiality} in read mode
					$$\mathtt{P3} ~\eqqdef \begin{array}{l}
						\forall~ \mathtt{\$p}=(\mathtt{\$f}, \mathtt{\$u})\in \mathtt{reading}, \forall~ \mathtt{\$p'}=(\mathtt{\$f'}, \mathtt{\$u'})\in \mathtt{writing} ~\cdot\\ \mathtt{\$un} = \mathtt{\$un'} \Longrightarrow \mathtt{\$ac_{f}'} \rhd \mathtt{\$ac_f}
					\end{array}$$
			\end{description}
		\end{block}
	\end{minipage}
	\hfill
	\begin{minipage}{0.49\textwidth}
		\begin{block}{4. Safe Iterative Evolution}
		\begin{minipage}{0.99\textwidth}
			An evolution step from an \textsc{Apn} $N$ into $N'$ consists of the two following steps: 
			\begin{enumerate}
				\item Building a morphism $f$ from $N$ to $N'$ (called a place-preserving morphism \cite{Padberg98rule-basedrefinement}) that respects the following conditions:
			\begin{itemize}
				\item Firing conditions are preserved;
				\item Places are preserved, i.e. no new arcs are mapped to mapped places;
				\item Mappings between places, transitions and algebraic signatures are injective; and signatures are correctly extended;
				\item $N'$ embeds $N$, meaning all arcs are mapped; 
			\end{itemize}
			\item Ensuring that firing conditions are strengthened (called a guard-strengthening morphism), i.e. conditions in $N'$ places semantically implies those in $N$;
			\end{enumerate}
		
		\bigskip\bigskip
		\textbf{We prove that invariant properties are preserved between $N$ and $N'$ if a place-preserving guard-strengthening morphism exist (cf. \cite{lucio:10}):}
				
		\begin{center}
		\textbf{$\mathtt{M}\models_{_{N}} \square\phi \Longrightarrow \mathtt{M'} \models_{_{N'}} \tau_f(\square\phi)$}
		\end{center}		
		\end{minipage}
		\end{block}
	\end{minipage}
\end{minipage}

\hfill

\begin{minipage}{0.98\textwidth}
	\begin{block}{5. Evolving the File System}
		\vspace{-0.5cm}
		\begin{minipage}[t]{0.3\textwidth}
			\begin{center}
				{\Large \textbf{Original File System $\FS$}}
			\end{center}
			
			\bigskip
			\begin{figure}%
				\includegraphics[scale=1.4]{figures/naive_fs.pdf}
			\end{figure}
			
			\bigskip
			\begin{center}
			No properties satisfied:\\
			$\FS \models \emptyset$
			\end{center}
			
		\end{minipage}
		\hfill
		\begin{minipage}[t]{0.3\textwidth}
			\begin{center}
				{\Large \textbf{Simple File System $\FSS$}}
			\end{center}
			
			\bigskip
			\begin{figure}%
				\includegraphics[scale=1.4]{figures/simple_fs.pdf}
			\end{figure}

			\bigskip
			\begin{center}
				\begin{itemize}
				\item Same Petri Net structure;
				\item Transition guards strengthened (in red)
			\end{itemize}
			
			\bigskip
			$\FSS \models \{ \mathtt{P1}, \mathtt{P2}\}$
			\end{center}
		\end{minipage}
		\hfill
		\begin{minipage}[t]{0.38\textwidth}
			\begin{center}
				{\Large \textbf{Confined File System $\FSC$}}
			\end{center}
			
			\bigskip
			\begin{figure}%
				\includegraphics[scale=1.4]{figures/confined_fs.pdf}
			\end{figure}
			
			\bigskip
			\begin{center}
				\begin{itemize}
				\item Two places added (in red);
				\item Transition guards also strengthened (in red).
				\end{itemize}
				
				\bigskip
				$\FSC \models \{ \mathtt{P1}, \mathtt{P2}, \mathtt{P3}\}$
			\end{center}
		\end{minipage}
	\end{block}
\end{minipage}

\hfill

\begin{minipage}{0.98\textwidth}
	\begin{minipage}{0.49\textwidth}
		\begin{block}{6. Conclusion and Future Work}
		\begin{minipage}{0.98\textwidth}
			\begin{itemize}
			\item Our work is a preliminary study on invariant preservation in iterative modeling
			\item A formal mathematical proof of the evolution conditions for invariant preservation is provided
			\item Our future research regards the preservation of other properties than invariants, e.g. liveness and other temporal properties
			\item We also wish to support the integration of our infrastructure with Domain-Specific Languages in general. Model transformations can be used too as a ``brigde'' to achieve this integration 
			\end{itemize}
			\medskip
			\vspace{0.2em}
		\end{minipage}
		\end{block}
	\end{minipage}
	\hfill
	\begin{minipage}{0.49\textwidth}
	\begin{block}{References}
		\begin{minipage}{0.98\textwidth}
			\small
			\bibliographystyle{IEEEtran}
			\bibliography{bibliography}
		\end{minipage}	
	\end{block}
\end{minipage}
\end{minipage}

\end{center}
\end{frame}

\end{document}